\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), $e$:es{-}E(${\it es}$).
\\[0ex]fischer\=\{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ (loc($e$) $\in$ $L$)
\\[0ex]$\Rightarrow$ (es{-}when(${\it es}$; mkid\{x:ut2\}; $e$) = mkid\{taken:ut2\} $\in$ Id)
\\[0ex]$\Rightarrow$ ($\neg$(es{-}after(${\it es}$; mkid\{x:ut2\}; $e$) = mkid\{taken:ut2\} $\in$ Id))
\\[0ex]$\Rightarrow$ guard(\=((es{-}after(${\it es}$; mkid\{x:ut2\}; $e$) = mkid\{free:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=(((es{-}tag(${\it es}$; $e$) = mkid\{free:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$)
\\[0ex]$\wedge$ ($\neg$($i$ = loc($e$)))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, loc($e$), mkid\{z:ut2\}$>$ $\in$ IdLnk))))
\-\\[0ex]$\wedge$ f{-}newround\=\{x:ut2, free:ut2, mine:ut2\}\+
\\[0ex](${\it es}$; $L$; es{-}sender(${\it es}$; $e$))))))
\-\-\-\-
\end{tabbing}